Language Tiers

Tier 1. Динамические языки программирования. JavaScript, Python, Erlang, Ruby, Elixir, К. Часто включают в себя макросы. Родоначальник семейства — LISP. Не-типизированное лямбда исчисление. Особенности устройства современной вычислительной техники со всем этими кешами, конвейерами и т.п. создали благоприятные условия для того, чтобы интерпретаторы иногда делали вид, что обходят компилируемые языки. Существуют два основных способа повышения производительности — это векторизация (K, Julia*) (или параллельная обработка) и трассирующая JIT компиляция (Lua, JVM*, V8). До сих пор бытует миф что эти языки молотят данные не хуже С++ кода. Ничем не примечательный Erlang берет в Tier 1 категории не бенчмарками но уровнем и культурой инфрастктуры, не смотря на возраст эквивалентный возрасту говна мамонта. Если вы сцыте от LISP машин то прибежище вы найдете только в Erlang. Smalltalk как лиспойобская ВМ судя по признакам подходит, но продакшин это не переживет.

Эта ниша удобна для создания референсных трастед виртуальных машин. Есть такая область их применения, причем даже не обязательно чтобы они работали супер-быстро, главное чтобы их верификация (третьими лицами или теорем пруверами) проходила максимально безболезненно. Представьте себе верифицировать средний LISP с 4-5 индуктивными конструкторами и верифицировать типизированные JVM или Julia. Хотят пейперы по интернету, что Java вообще не поддается верификации также как и С++.

Поэтому эту детскую категорию, где почти все имплементации с нормальным порядком редукции, нельзя сбрасывать со счетов и она всегда будет актуальной. Простейшие интерпретаторы — это ядра трастед вычислительных сред. По крайнем мере это качество в них очень легко развить.

Верифицировать Erlang нет никакого желания и возможности, поэтому нужно было найти какой-то интерпретирующее ядро, которое А) можно полностью самому надизайнить создав предусловия для безболезненной верификации Б) сделать это на языке максимально близкому к MLTT с индуктивными и коиндуктивными типами. Семантика Rust вполне подходит в качестве более продвинутый ML конфигурации, фактически когда мы говорим Rust мы имеем ввиду современный LLVM уровня ML в который еще и обогатили MLton-новским region-based memory allocation статическим анализом. Такой себе OCaml только без gc.

Tier 2. System F языки. Минимальный индустриальный базис. Все современные языки так или иначе сравнялись с этой системой. Morte/OM примеры современных тайпчекеров-компиляторов-экстракторов чистых рекурсивных и корекурсивных программ. Эта система достаточно мощная чтобы на ней составить трамплин для вычисления функторов локальных ДЗК. Этому исследовательскому проекту была посвящена суть категорных кодировок. Выражая эту идею простыми словами — создать вычислитель лимитов (обычный интерпретатор на свободных монадах), с помощью которого можно построить индуктивные и коиндуктивные типы по сигнатурам их алгебр. Достаточно мощная и новая идея к сожалению не была воспринята общественностью. Верифицированный System F компилятор не думаю что возможен, хотя ходили слухи о метациркулярности в Fw. Программы доказываются по другому, просто экспортируются в Coq/Agda и там для проимпорченых термов строятся общие высказывания. Так делались все прувед стеки: seL4, VST; и это пример того как делать не нужно.

Поэтому, чтобы минимизировать этот импорт к нулю нужно просто совместить Tier 2 и Tier 3 в один язык. Базовая библиотека таким образом распадается на части экстракт-имплементация (System F) и теоремы-спецификации (MLTT). Так произошло разделение OM и EXE. OM -- это программы ядра которые прошивается в трастед окружение: FPGA (Tier 0), или Tier 1. А EXE это язык на котором эти программы были сформулированы вместе с их спецификациями.

OM поддерживает сейчас Erlang бекенд, но Erlang -- это трастед интепретатор, нужен какой-то интерпретатор, который можно было поместить в узкие рамки (как спецификацию так и имплментацию), которые потом портировав на Coq можно было бы превратить в доказанную вычислительную среду уровня Tier 1. Такой кандидат — новая платформа на языке О. Ближайшие пол года год я буду посвящен исключительно языку О и его интерпретатору.

Tier 3. Теорем пруверы способные схавать HoTT, т.е. с бесконечной предикативной иерархией универсумов. Основное предназначение этого высшего Tier 3 — это доказательство свойств программ написанных на Tier 2. Процесс экстракта начинается с этого уровня и здесь тоже хочется чтобы в стеке небыло никаких импортов. Irdis, Agda, Coq, Lean, есть куча всего создать конкурентно-способный прувер это дело техники. Наработки Groupoid Infinity хоть и скромные но убедительные.

Таким образом в непрерывном стеке я выделяю только три языка: 1) виртуальная машина и нетипизированное лямбда исчисление; 2) System F промышленная базовая библиотека 3) язык доказывающий базовую библиотеку в продолжении синтаксиса языка уровня 2.

_______________
* Julia и JVM типизированные